{-
 -  Separ, Type/Eval.hs
 -
 -  Copyright (c) 2010 Dariusz Leniowski. All Rights Reserved.
 -
 -  Redistribution and use in source and binary forms, with or without 
 -  modification, are permitted provided that the following conditions 
 -  are met:
 -
 -  1. Redistributions of source code must retain the above copyright 
 -     notice, this list of conditions and the following disclaimer.
 -
 -  2. Redistributions in binary form must reproduce the above copyright 
 -     notice, this list of conditions and the following disclaimer 
 -     in the documentation and/or other materials provided with 
 -     the distribution.
 -
 -  3. The name of the author may not be used to endorse or promote 
 -     products derived from this software without specific prior 
 -     written permission.
 -
 -  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 
 -  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 
 -  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS 
 -  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL 
 -  THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, 
 -  INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES 
 -  (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS 
 -  OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) 
 -  HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, 
 -  STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING 
 -  IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 
 -  POSSIBILITY OF SUCH DAMAGE.
 -
 -}

-- Module Eval
-- Evaluation (instances of class Evaluable)
-- nothing else here (there's simplify and unify, but they
--   do nothing)

module Type.Eval where

import Prelude hiding (gcd,log)
import Control.Monad

import Type.Base hiding (value)
import Type.Lattice
import Type.Satisfiability

-------------------------------------------------
-- EVAL and SIMPLIFY
-------------------------------------------------
--
-- the main function
-- this is main aim
--
-- class Evaluable a where
--     eval :: a -> MM a
--

instance Evaluable Type where
	eval (Cls c) = return (Cls c)
	eval (Ref r) = do
		free <- isVarFree r
		if free then return (Ref r) else do
			value <- getVarValue r
			eval value
	eval (Lca a b) = do
		a' <- eval a
		b' <- eval b
		lca a' b' >>= simplify
	eval (Gcd a b) = do
		a' <- eval a
		b' <- eval b
		gcd a' b' >>= simplify
	eval (Lam b a r) = do
		simplify (Lam b a r)
	eval (Var r b f t) = do
		(u,i) <- unquantify True (Var r b f t)
		u' <- eval u
		quantify i u' >>= simplify
		-- simplify (Var r b f t)
	eval (PSet t n v) = do
		t' <- eval t
		v' <- eval v
		return $ pSet t' n v'
	eval (PGet t n) = eval t >>= evalProperty n >>= eval
	eval (App b f x) = do
		f' <- eval f
		x' <- eval x
		(a,r,li) <- makeLam False b f'
		unify a x'
		r0 <- eval r
		r1 <- quantify li r0
		simplify r1 >>= eval
	
-- second to eval
-- needed for types to be simpler
-- actualy just normalizes, optimizes bounds and calls

simplify :: Type -> MM Type
simplify t0 = do
	t1 <- normaloop t0 (return ())
	ctx <- getCtx
	guard (exists ctx t1)
	return t1

-----------------------------------------------
-- UNIFY
-----------------------------------------------
--
-- this function should be important
-- but it is so short (all the things are being done elsewhere)
-- therefore
-- TODO do I really need this? (why not just inline into eval)
--

unify :: Type -> Type -> MM ()
unify a b = do
	i <- pushEq TT
	-- WARNING b a -- reversed order of arguments
	uniLeq i True b a $ uniLoopK $ return () 
	f <- popEq i
	--when (isNotTT f) $ shw ("u",f) -- TODO take care of the rest
	ensure f
	when (isFF f) $ fail "unify got FF" 
	where
		isFF FF = True
		isFF _  = False
		isNotTT TT = False
		isNotTT _  = True

